package choco.integer.constraints;

import choco.mem.IStateInt;
import choco.integer.IntDomainVar;
import choco.*;

/**
 * A constraint to enforce Sigma_i coef[i]*x_i + k OP y_i where :
 * - OP belongs to >=, <=, =
 * - k is a constant
 * - x_i are boolean variable
 * - t_i is an enum variable
 * It improves the general IntLinComb by storing lower and upper bound of the expression
 * and sorting coefficient for filtering.
 * User: Hadrien
 * Date: 29 oct. 2006
 */
public class BoolIntLinComb extends AbstractLargeIntConstraint {

    /**
     * Field representing the type of linear constraint
     * (equality, inequality, disequality).
     */
    protected int op = -1;

    /**
     * Lower bound of the expression
     */
    protected IStateInt lb;

    /**
     * upper bound of the expression
     */
    protected IStateInt ub;


    /**
     * index of the maximum coefficient of positive sign
     */
    protected IStateInt maxPosCoeff;

    /**
     * index of the maximum coefficient of negative sign
     */
    protected IStateInt maxNegCoeff;

    /**
     * coefs and vars are sorted in increasing value of the coef
     */
    protected int[] sCoeffs;

    /**
     * number of negative coefficients
     */
    protected int nbNegCoef;

    /**
     * coefficients of the integer variable
     */
    protected int objCoef;

    /**
     * coefficients of the integer variable
     */
    protected int addcste;

    /**
     * One need to know what are the domain states we took into account during
     * the initial awake as we can receive the instantiation events then
     * this desynchronized domain copy is only maintained in the propagate !
     */
    protected choco.mem.IStateBitSet initCopy;

    public static IntDomainVar[] makeTableVar(IntDomainVar[] vs, IntDomainVar v) {
        IntDomainVar[] nvars = new IntDomainVar[vs.length + 1];
        System.arraycopy(vs, 0, nvars, 0, vs.length);
        nvars[vs.length] = v;
        return nvars;
    }


    /**
     * Constructs the constraint with the specified variables and constant.
     * Use the Problem.createIntLinComb API instead of this constructor.
     * WARNING : This constructor assumes :
     * - there are no null coefficient
     * - coefficients "coefs" are sorted from the smallest to the biggest (negative coefs first).
     * - objcoef is strictly POSITIVE
     * - op belongs to EQ, GT, NEQ and LEQ
     */
    public BoolIntLinComb(IntDomainVar[] vs, int[] coefs, IntDomainVar c, int objcoef, int scste, int op) {
        super(makeTableVar(vs, c));
        this.sCoeffs = coefs;
        this.op = op;
        this.cste = vs.length;
        this.objCoef = objcoef;
        this.addcste = scste;
        this.problem = vars[0].getProblem();
        nbNegCoef = 0;
        while (nbNegCoef < cste && sCoeffs[nbNegCoef] < 0) {
            nbNegCoef++;
        }
        if (op == IntLinComb.EQ || op == IntLinComb.GEQ || op == IntLinComb.LEQ) {
            this.maxPosCoeff = problem.getEnvironment().makeInt();
            this.maxNegCoeff = problem.getEnvironment().makeInt();
        }
        if (op == IntLinComb.EQ || op == IntLinComb.GEQ) {
            this.ub = problem.getEnvironment().makeInt();
        }
        if (op == IntLinComb.EQ || op == IntLinComb.LEQ) {
            this.lb = problem.getEnvironment().makeInt();
        }
        initCopy = problem.getEnvironment().makeBitSet(vars.length);
        //TODO NEQ
    }


    public static int divCeil(int a, int b) {
        return (int) Math.ceil((double) a / (double) b);
    }

    public static int divFloor(int a, int b) {
        return (int) Math.floor((double) a / (double) b);
    }

    public int getInfRight() {
        return objCoef * vars[cste].getInf();
    }

    public int getSupRight() {
        return objCoef * vars[cste].getSup();
    }

    public int getNewInfForObj() {
        return divCeil(lb.get(), objCoef);
    }

    public int getNewSupForObj() {
        return divFloor(ub.get(), objCoef);
    }

    /************************************************************************/
    /************** update of data structures *******************************/
    /**
     * ********************************************************************
     */

    public void updateUbLbOnInst(int idx, int i) {
        if (sCoeffs[idx] < 0) {
            if (i == 1) {
                ub.add(sCoeffs[idx]);
            } else {
                lb.add(-sCoeffs[idx]);
            }
        } else {
            if (i == 1) {
                lb.add(sCoeffs[idx]);
            } else {
                ub.add(-sCoeffs[idx]);
            }
        }
    }

    public void lookForNewMaxPosCoeff() {
        int i = maxPosCoeff.get() - 1;
        while (i >= nbNegCoef && vars[i].isInstantiated()) {
            i--;
        }
        maxPosCoeff.set(i);
    }

    public void lookForNewMaxNegCoeff() {
        int i = maxNegCoeff.get() + 1;
        while (i < nbNegCoef && vars[i].isInstantiated()) {
            i++;
        }
        maxNegCoeff.set(i);
    }

    /************************************************************************/
    /************** Main methods for filtering ******************************/
    /**
     * ********************************************************************
     */

    public boolean updateForGEQ() throws ContradictionException {
        boolean change = false;
        change |= filterPosCoeffUb();
        change |= filterNegCoeffUb();
        return change;
    }

    public boolean updateForLEQ() throws ContradictionException {
        boolean change = false;
        change |= filterPosCoeffLb();
        change |= filterNegCoeffLb();
        return change;
    }

    public void fixPointOnEQ() throws ContradictionException {
        boolean fixpoint = true;
        while (fixpoint) {
            fixpoint = false;
            vars[cste].updateSup(getNewSupForObj(), cIndices[cste]);
            vars[cste].updateInf(getNewInfForObj(), cIndices[cste]);
            fixpoint |= updateForGEQ();
            fixpoint |= updateForLEQ();
        }
    }

    /************************************************************************/
    /************** filtering based on the upperbound of the expression *****/
    /**
     * ********************************************************************
     */

    public boolean filterNegCoeffUb() throws ContradictionException {
        boolean change = false;
        int cpt = maxNegCoeff.get();
        while (cpt < nbNegCoef && vars[cpt].isInstantiated()) {
            cpt++;
        }
        while (cpt < nbNegCoef && ub.get() + sCoeffs[cpt] < getInfRight()) {
            vars[cpt].instantiate(0, cIndices[cpt]);
            change = true;
            if (op == IntLinComb.EQ)
                lb.add(-sCoeffs[cpt]);
            do {
                cpt++;
            } while (cpt < nbNegCoef && vars[cpt].isInstantiated());
        }
        maxNegCoeff.set(cpt);
        return change;
    }

    public boolean filterPosCoeffUb() throws ContradictionException {
        boolean change = false;
        int cpt = maxPosCoeff.get();
        while (cpt >= nbNegCoef && vars[cpt].isInstantiated()) {
            cpt--;
        }
        while (cpt >= nbNegCoef && ub.get() - sCoeffs[cpt] < getInfRight()) {
            vars[cpt].instantiate(1, cIndices[cpt]);
            change = true;
            if (op == IntLinComb.EQ)
                lb.add(sCoeffs[cpt]);
            do {
                cpt--;
            } while (cpt >= nbNegCoef && vars[cpt].isInstantiated());
        }
        maxPosCoeff.set(cpt);
        return change;
    }

    /************************************************************************/
    /************** filtering based on the lower bound of the expression ****/
    /**
     * ********************************************************************
     */

    public boolean filterPosCoeffLb() throws ContradictionException {
        boolean change = false;
        int cpt = maxPosCoeff.get();
        while (cpt >= nbNegCoef && vars[cpt].isInstantiated()) {
            cpt--;
        }
        while (cpt >= nbNegCoef && lb.get() + sCoeffs[cpt] > getSupRight()) {
            vars[cpt].instantiate(0, cIndices[cpt]);
            change = true;
            if (op == IntLinComb.EQ)
                ub.add(-sCoeffs[cpt]);
            do {
                cpt--;
            } while (cpt >= nbNegCoef && vars[cpt].isInstantiated());
        }
        maxPosCoeff.set(cpt);
        return change;
    }

    /**
     * enforce variables that would otherwise make the upper bound unreachable
     */
    public boolean filterNegCoeffLb() throws ContradictionException {
        boolean change = false;
        int cpt = maxNegCoeff.get();
        while (cpt < nbNegCoef && vars[cpt].isInstantiated()) {
            cpt++;
        }
        while (cpt < nbNegCoef && lb.get() - sCoeffs[cpt] > getSupRight()) {
            vars[cpt].instantiate(1, cIndices[cpt]);
            change = true;
            if (op == IntLinComb.EQ)
                ub.add(sCoeffs[cpt]);
            do {
                cpt++;
            } while (cpt < nbNegCoef && vars[cpt].isInstantiated());
        }
        maxNegCoeff.set(cpt);
        return change;
    }

    /************************************************************************/
    /************** React on event of the constraint ************************/
    /**
     * ********************************************************************
     */

    public void awakeOnInst(int idx) throws ContradictionException {
        //System.out.println("inst " + vars[idx] + " to val " + vars[idx].getVal()); // + "[" + lb.get() + " -- " + ub.get() + "]" + " =  [" + vars[cste].getInf() + " -- " + vars[cste].getSup() + "]");
        if (idx < cste) {
            int i = vars[idx].getVal();
            if (!initCopy.get(idx)) {
                if (op == IntLinComb.GEQ) {
                    if (sCoeffs[idx] < 0 && i == 1) {
                        ub.add(sCoeffs[idx]);
                        vars[cste].updateSup(getNewSupForObj(), cIndices[cste]);
                        updateForGEQ();
                    } else if (sCoeffs[idx] > 0 && i == 0) {
                        ub.add(-sCoeffs[idx]);
                        vars[cste].updateSup(getNewSupForObj(), cIndices[cste]);
                        updateForGEQ();
                    } else if (idx == maxPosCoeff.get()) {
                        lookForNewMaxPosCoeff();
                    } else if (idx == maxNegCoeff.get()) {
                        lookForNewMaxNegCoeff();
                    }
                } else if (op == IntLinComb.LEQ) {
                    if (sCoeffs[idx] > 0 && i == 1) {
                        lb.add(sCoeffs[idx]);
                        vars[cste].updateInf(getNewInfForObj(), cIndices[cste]);
                        updateForLEQ();
                    } else if (sCoeffs[idx] < 0 && i == 0) {
                        lb.add(-sCoeffs[idx]);
                        vars[cste].updateInf(getNewInfForObj(), cIndices[cste]);
                        updateForLEQ();
                    } else if (idx == maxPosCoeff.get()) {
                        lookForNewMaxPosCoeff();
                    } else if (idx == maxNegCoeff.get()) {
                        lookForNewMaxNegCoeff();
                    }
                    //updateForLEQ();
                } else if (op == IntLinComb.EQ) {
                    updateUbLbOnInst(idx, i);
                    fixPointOnEQ();
                } else {
                    //TODO
                }
            }
        } else {
            if (op == IntLinComb.GEQ) {
                filterPosCoeffUb();
                filterNegCoeffUb();
            } else if (op == IntLinComb.EQ) {
                fixPointOnEQ();
            } else if (op == IntLinComb.LEQ) {
                filterPosCoeffLb();
                filterNegCoeffLb();
            } else {
                //TODO
            }
        }
    }

    // can only be called on idx = cste
    public void awakeOnInf(int idx) throws ContradictionException {
        if (op == IntLinComb.GEQ) {
            filterPosCoeffUb();
            filterNegCoeffUb();
        } else if (op == IntLinComb.EQ) {
            fixPointOnEQ();
        } else {
            //TODO
        }
    }

    // can only be called on idx = cste
    public void awakeOnSup(int idx) throws ContradictionException {
        if (op == IntLinComb.EQ) {
            fixPointOnEQ();
        } else if (op == IntLinComb.LEQ) {
            filterPosCoeffLb();
            filterNegCoeffLb();
        } else {
            //TODO
        }
    }

    public void propagate() throws ContradictionException {
        if (op == IntLinComb.EQ) {
            propagateEQ();
        } else if (op == IntLinComb.GEQ) {
            propagateGEQ();
        } else if (op == IntLinComb.LEQ) {
            propagateLEQ();
        } else {
            //TODO
        }
    }

    public void propagateEQ() throws ContradictionException {
        for (int i = 0; i < nbNegCoef; i++) {
            if (ub.get() + sCoeffs[i] < getInfRight())
                vars[i].instantiate(0, cIndices[i]);
        }
        for (int i = nbNegCoef; i < cste; i++) {
            if (ub.get() - sCoeffs[i] < getInfRight())
                vars[i].instantiate(1, cIndices[i]);
        }
        for (int i = 0; i < nbNegCoef; i++) {
            if (lb.get() - sCoeffs[i] > getSupRight())
                vars[i].instantiate(1, cIndices[i]);
        }
        for (int i = nbNegCoef; i < cste; i++) {
            if (lb.get() + sCoeffs[i] > getSupRight())
                vars[i].instantiate(0, cIndices[i]);
        }
        for (int i = 0; i < cste; i++) {
            if (vars[i].isInstantiated()) {
                updateUbLbOnInst(i, vars[i].getVal());
                initCopy.set(i);
            }
        }
        fixPointOnEQ();
        vars[cste].updateInf(getNewInfForObj(), cIndices[cste]);
        vars[cste].updateSup(getNewSupForObj(), cIndices[cste]);
    }

    public void propagateGEQ() throws ContradictionException {
        for (int i = 0; i < nbNegCoef; i++) {
            if (ub.get() + sCoeffs[i] < getInfRight())
                vars[i].instantiate(0, cIndices[i]);
            if (vars[i].isInstantiated()) {
                awakeOnInst(i);
                initCopy.set(i);
            }
        }
        for (int i = nbNegCoef; i < cste; i++) {
            if (ub.get() - sCoeffs[i] < getInfRight())
                vars[i].instantiate(1, cIndices[i]);
            if (vars[i].isInstantiated()) {
                awakeOnInst(i);
                initCopy.set(i);
            }
        }
        //System.out.println("update sup de " + vars[cste] + " a " + divFloor(ub.get(), objCoef));
        vars[cste].updateSup(getNewSupForObj(), cIndices[cste]);
        updateForGEQ();
    }

    public void propagateLEQ() throws ContradictionException {
        for (int i = 0; i < nbNegCoef; i++) {
            if (lb.get() - sCoeffs[i] > getSupRight())
                vars[i].instantiate(1, -1);
            if (vars[i].isInstantiated()) {
                awakeOnInst(i);
                initCopy.set(i);
            }
        }
        for (int i = nbNegCoef; i < cste; i++) {
            if (lb.get() + sCoeffs[i] > getSupRight())
                vars[i].instantiate(0, -1);
            if (vars[i].isInstantiated()) {
                awakeOnInst(i);
                initCopy.set(i);
            }
        }
        vars[cste].updateInf(getNewInfForObj(), cIndices[cste]);
        updateForLEQ();
    }

    public void awake() throws ContradictionException {
        for (int i = 0; i < vars.length; i++) {
            initCopy.clear(i);                       
        }
        if (op == IntLinComb.GEQ || op == IntLinComb.EQ || op == IntLinComb.LEQ) {
            maxNegCoeff.set(0);
            maxPosCoeff.set(cste - 1);
        }
        if (op == IntLinComb.GEQ || op == IntLinComb.EQ) {
            initUb();
        }
        if (op == IntLinComb.EQ || op == IntLinComb.LEQ) {
            initlb();
        }
        if (op == IntLinComb.NEQ) {
            //TODO
        }
        propagate();
    }

    public void initUb() {
        int upb = addcste;
        for (int i = 0; i < sCoeffs.length; i++) {
            if (sCoeffs[i] > 0)
                upb += sCoeffs[i];
        }
        ub.set(upb);
    }

    public void initlb() {
        int lpb = addcste;
        for (int i = 0; i < sCoeffs.length; i++) {
            if (sCoeffs[i] < 0)
                lpb += sCoeffs[i];
        }
        lb.set(lpb);
    }

    /**
     * Tests if the constraint is consistent
     * with respect to the current state of domains.
     *
     * @return true iff the constraint is bound consistent
     *         (weaker than arc consistent)
     */
    public boolean isConsistent() {
        if (op == IntLinComb.EQ) {
            return (hasConsistentLowerBound() && hasConsistentUpperBound());
        } else if (op == IntLinComb.GEQ) {
            return hasConsistentUpperBound();
        } else if (op == IntLinComb.LEQ) {
            return hasConsistentLowerBound();
        }
        return true;
    }

    /**
     * Tests if the constraint is consistent
     * with respect to the current state of domains.
     *
     * @return true iff the constraint is bound consistent
     *         (weaker than arc consistent)
     */
    protected boolean hasConsistentUpperBound() {
        if (ub.get() < getInfRight()) {
            return false;
        } else {
            for (int i = 0; i < nbNegCoef; i++) {
                if (ub.get() + vars[i].getSup() * sCoeffs[i] < getInfRight()) {
                    return false;
                }
            }
            for (int i = nbNegCoef; i < cste; i++) {
                if (ub.get() - vars[i].getInf() * sCoeffs[i] < getInfRight()) {
                    return false;
                }
            }
            return true;
        }
    }

    /**
     * Tests if the constraint is consistent
     * with respect to the current state of domains.
     *
     * @return true iff the constraint is bound consistent
     *         (weaker than arc consistent)
     */
    protected boolean hasConsistentLowerBound() {
        if (lb.get() > getSupRight()) {
            return false;
        } else {
            for (int i = 0; i < nbNegCoef; i++) {
                if (lb.get() - vars[i].getInf() * sCoeffs[i] > getSupRight()) {
                    return false;
                }
            }
            for (int i = nbNegCoef; i < cste; i++) {
                if (lb.get() + vars[i].getSup() * sCoeffs[i] > getSupRight()) {
                    return false;
                }
            }
            return true;
        }
    }

    /**
     * Checks if the constraint is entailed.
     *
     * @return Boolean.TRUE if the constraint is satisfied, Boolean.FALSE if it
     *         is violated, and null if the filtering algorithm cannot infer yet.
     */
    public Boolean isEntailed() {
        if (op == IntLinComb.EQ) {
            int lb = computeLbFromScratch();
            int ub = computeUbFromScratch();
            int cstelb = objCoef*vars[cste].getInf();
            int csteub = objCoef*vars[cste].getSup();
            if (lb > csteub || ub < cstelb) {
                return Boolean.FALSE;
            } else if (lb == ub &&
                       vars[cste].isInstantiated() &&
                       objCoef * vars[cste].getVal() == lb) {
                return Boolean.TRUE;
            } else return null;
        } else if (op == IntLinComb.GEQ) {
            if (computeLbFromScratch() >= getSupRight()) {
                return Boolean.TRUE;
            } else if (computeUbFromScratch() < getInfRight()) {
                return Boolean.FALSE;
            } else return null;
        } else if (op == IntLinComb.LEQ) {
            if (computeUbFromScratch() <= getInfRight()) {
                return Boolean.TRUE;
            } else if (computeLbFromScratch() > getSupRight()) {
                return Boolean.FALSE;
            } else return null;
        } else {
            throw new Error("NEQ not managed by boolIntLinComb");
        }
    }

    public boolean isSatisfied() {
        int exp = 0;
        for (int i = 0; i < cste; i++) {
            exp += vars[i].getVal() * sCoeffs[i];
        }
        if (op == IntLinComb.GEQ) {
            return exp + addcste >= objCoef * vars[cste].getVal();
        } else if (op == IntLinComb.LEQ) {
            return exp + addcste <= objCoef * vars[cste].getVal();
        } else if (op == IntLinComb.EQ) {
            return exp + addcste == objCoef * vars[cste].getVal();
        } else if (op == IntLinComb.NEQ) {
            return exp + addcste != objCoef * vars[cste].getVal();
        } else {
            throw new Error("operator unknown for BoolIntLinComb");
        }
    }

  public String pretty() {
    StringBuilder sb = new StringBuilder();
    for (int i = 0; i < cste; i++) {
      if (i > 0) sb.append(" + ");
      sb.append(sCoeffs[i]).append("*").append(vars[i].pretty());
    }
    sb.append(" + ").append(addcste);
    switch (op) {
      case IntLinComb.GEQ: sb.append(" >= "); break;
      case IntLinComb.LEQ: sb.append(" <= "); break;
      case IntLinComb.EQ: sb.append(" = "); break;
      case IntLinComb.NEQ: sb.append(" != "); break;
      default: sb.append(" ??? "); break;
    }
    sb.append(objCoef).append("*").append(vars[cste].pretty());
    return sb.toString();
  }

    /**
     * Computes the opposite of this constraint.
     *
     * @return a constraint with the opposite semantic
     */
    public AbstractConstraint opposite() {
        IntDomainVar[] bvs = new IntDomainVar[cste];
        System.arraycopy(vars, 0, bvs, 0, cste);
        if (op == IntLinComb.EQ) {
            IntDomainVar[] vs = new IntDomainVar[vars.length];
            System.arraycopy(vars, 0, vs, 0, vars.length);
            int[] coeff = new int[cste + 1];
            System.arraycopy(sCoeffs, 0, coeff, 0, cste);
            coeff[cste] = -objCoef;
            return (AbstractConstraint) problem.neq(problem.scalar(vs, coeff), -addcste);
            //throw new Error("NEQ not yet implemented in BoolIntLinComb for opposite");
        } else if (op == IntLinComb.NEQ) {
            return new BoolIntLinComb(bvs, sCoeffs, vars[cste], objCoef, addcste, IntLinComb.EQ);
        } else if (op == IntLinComb.GEQ) {
            return new BoolIntLinComb(bvs, sCoeffs, vars[cste], objCoef, addcste + 1, IntLinComb.LEQ);
        } else if (op == IntLinComb.LEQ) {
            return new BoolIntLinComb(bvs, sCoeffs, vars[cste], objCoef, addcste - 1, IntLinComb.GEQ);
        } else {
            throw new Error("operator unknown for BoolIntLinComb");
        }
    }

    /**
     * Computes an upper bound estimate of a linear combination of variables.
     *
     * @return the new upper bound value
     */
    protected int computeUbFromScratch() {
        int s = addcste;
        int i;
        for (i = 0; i < nbNegCoef; i++) {
            s += (vars[i].getInf() * sCoeffs[i]);
        }
        for (i = nbNegCoef; i < cste; i++) {
            s += (vars[i].getSup() * sCoeffs[i]);
        }
        return s;
    }

    /**
     * Computes a lower bound estimate of a linear combination of variables.
     *
     * @return the new lower bound value
     */
    protected int computeLbFromScratch() {
        int s = addcste;
        int i;
        for (i = 0; i < nbNegCoef; i++) {
            s += (vars[i].getSup() * sCoeffs[i]);
        }
        for (i = nbNegCoef; i < cste; i++) {
            s += (vars[i].getInf() * sCoeffs[i]);
        }
        return s;
  }
}
